T:Type, L:T List, P:({x:T| (x  L) }Prop). xL.P(x)  (xL. P(x)) 

latex

Definitions	x(s), xL. P(x), xL.P(x), P  Q, Prop, x:A. B(x), t  T, x. t(x), True, P  Q, P  Q, P & Q, (x  l), strong-subtype(A;B), ||as||, False, A, AB, , A & B, l[i], x:A. B(x), {T}, SQType(T)
Lemmas	nat wf, length wf1, select wf, strong-subtype-l member, strong-subtype-set3, strong-subtype-self, list-subtype, iff functionality wrt iff, l all cons, l-all wf, l member wf, true wf, l all wf, l all nil